Nuprl Lemma : left_child_wf
4,23
postcript
pdf
E
:Type,
t
:Tree(
E
). left_child(
t
)
Tree(
E
)
latex
Definitions
left_child(
t
)
,
Tree(
E
)
,
tree_con(
E
;
T
)
,
Default =>
body
,
Case(
value
)
body
,
Case
x
;
y
=>
body
(
x
;
y
)
cont
,
{
T
}
,
tree_leaf(
x
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
tree
leaf
wf2
,
tree
wf
origin
E:Type, t:Tree(E). left_child(t) 
Tree(E) E:Type, t:Tree(E). left_child(t) Tree(E) x:A. B(x) T